shubhamkumar13

#lang racket

(require test-engine/racket-tests)

; file contains Unicode characters - download rather than cut/paste from browser

;; proust-prop-imp-basic: minimal proof assistant for implicational fragment of propositional logic
;; Prabhakar Ragde (April 2020)

;; Can only check full proof terms, no incremental interactive building here

shubhamkumar13

module vec where

open import Data.Product hiding (zip)

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

data Vec (X : Set) : ℕ → Set where
  ⟨⟩  : Vec X zero

shubhamkumar13

# dict1 : {
#     "a" : 1,
#     "b" : "3",
#     "c" : (4,),
#     "d" : [3],
#     "e" : {"f" : 7},
# }
# dict2 : {
#     "a" : 2,
#     "b" : "4",

shubhamkumar13

use std::collections::VecDeque;
use std::panic;

trait FP<T> {
    fn cons(self, x : T) -> VecDeque<T>;
    fn snoc(self, x : T) -> VecDeque<T>;
    fn tail(self) -> Option<VecDeque<T>>;
    fn init(self) -> Option<VecDeque<T>>;
    fn head(self) -> Option<T>;
    fn last(self) -> Option<T>;

shubhamkumar13

section
  abbrev Stack := List Int

  def nAdd (s : Stack) (pc : Nat) : Stack × Nat :=
    match s with
    | [] => ([], pc)
    | x :: [] => ([x], pc)
    | x :: y :: xs => ((x + y) :: xs, pc + 1)
  
  def nSub (s : Stack) (pc : Nat) : Stack × Nat :=

shubhamkumar13

 // update cab destination and person_id
    nearest_cab.update_destination(Some(person.location.clone()));
    nearest_cab.update_person_id(ObjectId::parse_str(person_id).ok());
    // update cab by using `assign_person`
    let cab_id = match nearest_cab.id {
        Some(obj_id) => obj_id.to_hex(),
        None => panic!("cannot get the cab id"),
    };
    let update_result = db.assign_person(&cab_id, nearest_cab.clone());
    // return result as person and cab tuple

shubhamkumar13

   // find the nearest cab in the fleet from the person
   let mut nearest_cab = fleet
        .into_iter()
        .filter(|x| is_free((*x).clone()).is_ok())
        .reduce(|c1, c2| person.nearest_cab(&c1, &c2))
        .and_then(|x| Some(x.clone()))
        .expect("Unable to get the nearest cab");

shubhamkumar13

    // find the nearest cab in the fleet from the person
       let mut nearest_cab = fleet
            .into_iter()
            .reduce(|c1, c2| person.nearest_cab(&c1, &c2))
            .and_then(|x| Some(x.clone()))
            .expect("Unable to get the nearest cab");
           
    // check if the cab is assigned or not
        match is_free(nearest_cab.clone()) {
            Ok(_) => {

shubhamkumar13

(let
 '(init_value, reachable) :=
  match entrypoints.(Script_typed_ir.entrypoints_node.at_node) with
  | Some e =>
      ((Map.Make Alpha_context.Entrypoint.T).(S.singleton)
       e.(Script_typed_ir.entrypoint_info.name) tt, true)
  | None => ((Map.Make Alpha_context.Entrypoint.T).(S.empty), false)
  end in
  let? ' (first_unreachable, all)

shubhamkumar13

diff --git a/src/sexp_conv.ml b/src/sexp_conv.ml
index ed2becf..406ee73 100644
--- a/src/sexp_conv.ml
+++ b/src/sexp_conv.ml
@@ -110,7 +110,7 @@ module Exn_converter = struct
   end
 
   let exn_id_map
-    : (Obj.Extension_constructor.t, Registration.t) Ephemeron.K1.t Exn_ids.t ref
+    : (Obj.Extension_constructor.t * Registration.t) Exn_ids.t ref